\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it Master}$:AbsInterface(chain\_master()),\+
\\[0ex]${\it Config}$:AbsInterface(chain\_config()), ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)),
\\[0ex]$u$:(\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} $\rightarrow$\{$e$:E$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Config}$))\} ).
\-\\[0ex]chain{-}replication\{i:l\}(${\it es}$;${\it Cmd}$;${\it Sys}$;${\it Config}$;${\it Master}$;$u$) $\in$ $\mathbb{P}$
\end{tabbing}